COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.CB PATTERNS IN SEQUENCE SOLITAIRE
C00005 ENDMK
C⊗;
.CB PATTERNS IN SEQUENCE SOLITAIRE


	Sequence solitaire provides a good domain in which to study
certain kinds of patterns.

	Consider first the blocking pattern.  A set of cards is blocked
in a situation if regardless of what the other cards turn out to be,
this set cannot be played.  We can define it as follows:


∀m s.(blocked(m,s) ≡ ∀a.(a ε 4↑m ∧ compatible(a,s) ⊃
	∀x.(xεm ⊃ ∃y.covers(y,x,s) ∨ ∃z.precedes(z,x,a))))

blocked(m,s) - the set m of cards is self-blocked in the situation s because
for every possible assignment a of the cards in m to final piles,
every card x in m is either covered by another card y in m that must
be removed first or preceded in the sequence defined by a by another
card z in m.

compatible(a,s) means that the assignment a of cards to final destinations
is compatible with the cards already played in situation s.

covers(y,x,s) means that card y is above card x in some storage pile
in situation s and hence must be played before x can be played.

precedes(z,x,a) means that in assignment a, the card z must go on
a final pile before the card x.

	The above is fine for predicate calculus proofs, but the
formalism is too general in that there doesn't (and cannot) exist
a pattern matching mechanism for such general patterns.  The first
step in getting a matchable pattern might be to make ⊗a explicit
in the pattern, i.e. to write

!!a2:	%2blocked1(m,s,a) ≡ aε4↑m ∧ compatible(a,s) ⊃
	∀x.(xεm ⊃ ∃y.covers(y,x,s) ∨ ∃z.precedes(z,x,a))%1.

	This pattern is still expressed in terms of a set ⊗m of cards.
Blocking patterns with a fixed
sized set and fixed pattern of covering and precedence are easier to
handle though less general.  The simplest example is

!!a3:	%2∀x y s.(blocked2(x,y,s) ≡ covers(y,x,s) 
		∧ ∀a.(a ε 4↑{x,y} ∧ compatible(a,s) ⊃ precedes(x,y,a)))%1.